0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 0 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 19 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 2079 ms)
↳10 BOUNDS(1, n^2)
half(0) → 0
half(s(0)) → 0
half(s(s(x))) → s(half(x))
le(0, y) → true
le(s(x), 0) → false
le(s(x), s(y)) → le(x, y)
inc(s(x)) → s(inc(x))
inc(0) → s(0)
logarithm(x) → logIter(x, 0)
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y))
if(false, b, x, y) → logZeroError
if(true, false, x, s(y)) → y
if(true, true, x, y) → logIter(x, y)
f → g
f → h
half(0) → 0 [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
logarithm(x) → logIter(x, 0) [1]
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) [1]
if(false, b, x, y) → logZeroError [1]
if(true, false, x, s(y)) → y [1]
if(true, true, x, y) → logIter(x, y) [1]
f → g [1]
f → h [1]
half(0) → 0 [1]
half(s(0)) → 0 [1]
half(s(s(x))) → s(half(x)) [1]
le(0, y) → true [1]
le(s(x), 0) → false [1]
le(s(x), s(y)) → le(x, y) [1]
inc(s(x)) → s(inc(x)) [1]
inc(0) → s(0) [1]
logarithm(x) → logIter(x, 0) [1]
logIter(x, y) → if(le(s(0), x), le(s(s(0)), x), half(x), inc(y)) [1]
if(false, b, x, y) → logZeroError [1]
if(true, false, x, s(y)) → y [1]
if(true, true, x, y) → logIter(x, y) [1]
f → g [1]
f → h [1]
| half :: 0:s:logZeroError → 0:s:logZeroError 0 :: 0:s:logZeroError s :: 0:s:logZeroError → 0:s:logZeroError le :: 0:s:logZeroError → 0:s:logZeroError → true:false true :: true:false false :: true:false inc :: 0:s:logZeroError → 0:s:logZeroError logarithm :: 0:s:logZeroError → 0:s:logZeroError logIter :: 0:s:logZeroError → 0:s:logZeroError → 0:s:logZeroError if :: true:false → true:false → 0:s:logZeroError → 0:s:logZeroError → 0:s:logZeroError logZeroError :: 0:s:logZeroError f :: g:h g :: g:h h :: g:h |
half(v0) → null_half [0]
le(v0, v1) → null_le [0]
inc(v0) → null_inc [0]
if(v0, v1, v2, v3) → null_if [0]
null_half, null_le, null_inc, null_if
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
0 => 0
true => 2
false => 1
logZeroError => 1
g => 0
h => 1
null_half => 0
null_le => 0
null_inc => 0
null_if => 0
f -{ 1 }→ 1 :|:
f -{ 1 }→ 0 :|:
half(z) -{ 1 }→ 0 :|: z = 0
half(z) -{ 1 }→ 0 :|: z = 1 + 0
half(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
half(z) -{ 1 }→ 1 + half(x) :|: x >= 0, z = 1 + (1 + x)
if(z, z', z'', z1) -{ 1 }→ y :|: z = 2, x >= 0, y >= 0, z'' = x, z1 = 1 + y, z' = 1
if(z, z', z'', z1) -{ 1 }→ logIter(x, y) :|: z = 2, z1 = y, z' = 2, x >= 0, y >= 0, z'' = x
if(z, z', z'', z1) -{ 1 }→ 1 :|: b >= 0, z1 = y, z = 1, x >= 0, y >= 0, z' = b, z'' = x
if(z, z', z'', z1) -{ 0 }→ 0 :|: z1 = v3, v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0, v3 >= 0
inc(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
inc(z) -{ 1 }→ 1 + inc(x) :|: x >= 0, z = 1 + x
inc(z) -{ 1 }→ 1 + 0 :|: z = 0
le(z, z') -{ 1 }→ le(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
le(z, z') -{ 1 }→ 2 :|: y >= 0, z = 0, z' = y
le(z, z') -{ 1 }→ 1 :|: x >= 0, z = 1 + x, z' = 0
le(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
logIter(z, z') -{ 1 }→ if(le(1 + 0, x), le(1 + (1 + 0), x), half(x), inc(y)) :|: x >= 0, y >= 0, z = x, z' = y
logarithm(z) -{ 1 }→ logIter(x, 0) :|: x >= 0, z = x
| eq(start(V, V2, V11, V12),0,[half(V, Out)],[V >= 0]). eq(start(V, V2, V11, V12),0,[le(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V11, V12),0,[inc(V, Out)],[V >= 0]). eq(start(V, V2, V11, V12),0,[logarithm(V, Out)],[V >= 0]). eq(start(V, V2, V11, V12),0,[logIter(V, V2, Out)],[V >= 0,V2 >= 0]). eq(start(V, V2, V11, V12),0,[if(V, V2, V11, V12, Out)],[V >= 0,V2 >= 0,V11 >= 0,V12 >= 0]). eq(start(V, V2, V11, V12),0,[f(Out)],[]). eq(half(V, Out),1,[],[Out = 0,V = 0]). eq(half(V, Out),1,[],[Out = 0,V = 1]). eq(half(V, Out),1,[half(V1, Ret1)],[Out = 1 + Ret1,V1 >= 0,V = 2 + V1]). eq(le(V, V2, Out),1,[],[Out = 2,V3 >= 0,V = 0,V2 = V3]). eq(le(V, V2, Out),1,[],[Out = 1,V4 >= 0,V = 1 + V4,V2 = 0]). eq(le(V, V2, Out),1,[le(V5, V6, Ret)],[Out = Ret,V2 = 1 + V6,V5 >= 0,V6 >= 0,V = 1 + V5]). eq(inc(V, Out),1,[inc(V7, Ret11)],[Out = 1 + Ret11,V7 >= 0,V = 1 + V7]). eq(inc(V, Out),1,[],[Out = 1,V = 0]). eq(logarithm(V, Out),1,[logIter(V8, 0, Ret2)],[Out = Ret2,V8 >= 0,V = V8]). eq(logIter(V, V2, Out),1,[le(1 + 0, V9, Ret0),le(1 + (1 + 0), V9, Ret12),half(V9, Ret21),inc(V10, Ret3),if(Ret0, Ret12, Ret21, Ret3, Ret4)],[Out = Ret4,V9 >= 0,V10 >= 0,V = V9,V2 = V10]). eq(if(V, V2, V11, V12, Out),1,[],[Out = 1,V13 >= 0,V12 = V14,V = 1,V15 >= 0,V14 >= 0,V2 = V13,V11 = V15]). eq(if(V, V2, V11, V12, Out),1,[],[Out = V16,V = 2,V17 >= 0,V16 >= 0,V11 = V17,V12 = 1 + V16,V2 = 1]). eq(if(V, V2, V11, V12, Out),1,[logIter(V18, V19, Ret5)],[Out = Ret5,V = 2,V12 = V19,V2 = 2,V18 >= 0,V19 >= 0,V11 = V18]). eq(f(Out),1,[],[Out = 0]). eq(f(Out),1,[],[Out = 1]). eq(half(V, Out),0,[],[Out = 0,V20 >= 0,V = V20]). eq(le(V, V2, Out),0,[],[Out = 0,V21 >= 0,V22 >= 0,V = V21,V2 = V22]). eq(inc(V, Out),0,[],[Out = 0,V23 >= 0,V = V23]). eq(if(V, V2, V11, V12, Out),0,[],[Out = 0,V12 = V24,V25 >= 0,V11 = V26,V27 >= 0,V = V25,V2 = V27,V26 >= 0,V24 >= 0]). input_output_vars(half(V,Out),[V],[Out]). input_output_vars(le(V,V2,Out),[V,V2],[Out]). input_output_vars(inc(V,Out),[V],[Out]). input_output_vars(logarithm(V,Out),[V],[Out]). input_output_vars(logIter(V,V2,Out),[V,V2],[Out]). input_output_vars(if(V,V2,V11,V12,Out),[V,V2,V11,V12],[Out]). input_output_vars(f(Out),[],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. non_recursive : [f/1]
1. recursive : [half/2]
2. recursive : [inc/2]
3. recursive : [le/3]
4. recursive : [if/5,logIter/3]
5. non_recursive : [logarithm/2]
6. non_recursive : [start/4]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into f/1
1. SCC is partially evaluated into half/2
2. SCC is partially evaluated into inc/2
3. SCC is partially evaluated into le/3
4. SCC is partially evaluated into logIter/3
5. SCC is completely evaluated into other SCCs
6. SCC is partially evaluated into start/4
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations f/1
* CE 28 is refined into CE [29]
* CE 27 is refined into CE [30]
### Cost equations --> "Loop" of f/1
* CEs [29] --> Loop 17
* CEs [30] --> Loop 18
### Ranking functions of CR f(Out)
#### Partial ranking functions of CR f(Out)
### Specialization of cost equations half/2
* CE 17 is refined into CE [31]
* CE 16 is refined into CE [32]
* CE 19 is refined into CE [33]
* CE 18 is refined into CE [34]
### Cost equations --> "Loop" of half/2
* CEs [34] --> Loop 19
* CEs [31] --> Loop 20
* CEs [32,33] --> Loop 21
### Ranking functions of CR half(V,Out)
* RF of phase [19]: [V-1]
#### Partial ranking functions of CR half(V,Out)
* Partial RF of phase [19]:
- RF of loop [19:1]:
V-1
### Specialization of cost equations inc/2
* CE 26 is refined into CE [35]
* CE 25 is refined into CE [36]
* CE 24 is refined into CE [37]
### Cost equations --> "Loop" of inc/2
* CEs [37] --> Loop 22
* CEs [35] --> Loop 23
* CEs [36] --> Loop 24
### Ranking functions of CR inc(V,Out)
* RF of phase [22]: [V]
#### Partial ranking functions of CR inc(V,Out)
* Partial RF of phase [22]:
- RF of loop [22:1]:
V
### Specialization of cost equations le/3
* CE 23 is refined into CE [38]
* CE 21 is refined into CE [39]
* CE 20 is refined into CE [40]
* CE 22 is refined into CE [41]
### Cost equations --> "Loop" of le/3
* CEs [41] --> Loop 25
* CEs [38] --> Loop 26
* CEs [39] --> Loop 27
* CEs [40] --> Loop 28
### Ranking functions of CR le(V,V2,Out)
* RF of phase [25]: [V,V2]
#### Partial ranking functions of CR le(V,V2,Out)
* Partial RF of phase [25]:
- RF of loop [25:1]:
V
V2
### Specialization of cost equations logIter/3
* CE 15 is refined into CE [42,43,44,45,46,47,48,49]
* CE 12 is refined into CE [50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101]
* CE 14 is refined into CE [102,103,104]
* CE 13 is refined into CE [105,106,107,108,109,110,111,112]
### Cost equations --> "Loop" of logIter/3
* CEs [112] --> Loop 29
* CEs [111] --> Loop 30
* CEs [110] --> Loop 31
* CEs [108] --> Loop 32
* CEs [107] --> Loop 33
* CEs [106] --> Loop 34
* CEs [109] --> Loop 35
* CEs [105] --> Loop 36
* CEs [62,66,74,78,82,86,94,98] --> Loop 37
* CEs [104] --> Loop 38
* CEs [103] --> Loop 39
* CEs [70,71,72,73,90,91,92,93,102] --> Loop 40
* CEs [42,43,44,45,46,47,48,49] --> Loop 41
* CEs [50,51,52,53,54,55,56,57,58,59,60,61,63,64,65,67,68,69,75,76,77,79,80,81,83,84,85,87,88,89,95,96,97,99,100,101] --> Loop 42
### Ranking functions of CR logIter(V,V2,Out)
* RF of phase [29,30,31,35]: [V-1]
#### Partial ranking functions of CR logIter(V,V2,Out)
* Partial RF of phase [29,30,31,35]:
- RF of loop [29:1,30:1,31:1,35:1]:
V-1
- RF of loop [35:1]:
-V2+1 depends on loops [29:1,31:1]
### Specialization of cost equations start/4
* CE 2 is refined into CE [113]
* CE 3 is refined into CE [114,115,116,117,118,119,120]
* CE 4 is refined into CE [121]
* CE 5 is refined into CE [122]
* CE 6 is refined into CE [123,124]
* CE 7 is refined into CE [125,126,127,128,129]
* CE 8 is refined into CE [130,131,132,133]
* CE 9 is refined into CE [134,135,136,137,138]
* CE 10 is refined into CE [139,140,141,142,143,144,145]
* CE 11 is refined into CE [146,147]
### Cost equations --> "Loop" of start/4
* CEs [113,114,115,116,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147] --> Loop 43
### Ranking functions of CR start(V,V2,V11,V12)
#### Partial ranking functions of CR start(V,V2,V11,V12)
Computing Bounds
=====================================
#### Cost of chains of f(Out):
* Chain [18]: 1
with precondition: [Out=0]
* Chain [17]: 1
with precondition: [Out=1]
#### Cost of chains of half(V,Out):
* Chain [[19],21]: 1*it(19)+1
Such that:it(19) =< 2*Out
with precondition: [Out>=1,V>=2*Out]
* Chain [[19],20]: 1*it(19)+1
Such that:it(19) =< 2*Out
with precondition: [V=2*Out+1,V>=3]
* Chain [21]: 1
with precondition: [Out=0,V>=0]
* Chain [20]: 1
with precondition: [V=1,Out=0]
#### Cost of chains of inc(V,Out):
* Chain [[22],24]: 1*it(22)+1
Such that:it(22) =< Out
with precondition: [V+1=Out,V>=1]
* Chain [[22],23]: 1*it(22)+0
Such that:it(22) =< Out
with precondition: [Out>=1,V>=Out]
* Chain [24]: 1
with precondition: [V=0,Out=1]
* Chain [23]: 0
with precondition: [Out=0,V>=0]
#### Cost of chains of le(V,V2,Out):
* Chain [[25],28]: 1*it(25)+1
Such that:it(25) =< V
with precondition: [Out=2,V>=1,V2>=V]
* Chain [[25],27]: 1*it(25)+1
Such that:it(25) =< V2
with precondition: [Out=1,V2>=1,V>=V2+1]
* Chain [[25],26]: 1*it(25)+0
Such that:it(25) =< V2
with precondition: [Out=0,V>=1,V2>=1]
* Chain [28]: 1
with precondition: [V=0,Out=2,V2>=0]
* Chain [27]: 1
with precondition: [V2=0,Out=1,V>=1]
* Chain [26]: 0
with precondition: [Out=0,V>=0,V2>=0]
#### Cost of chains of logIter(V,V2,Out):
* Chain [[29,30,31,35],42]: 8*it(29)+11*it(30)+6*it(35)+11*s(4)+11*s(5)+56*s(18)+12*s(41)+12*s(62)+3*s(143)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+5
Such that:aux(14) =< 1
aux(15) =< 2
aux(21) =< V+V2
aux(17) =< V/2+V2+1
aux(18) =< V/2+V2+2
aux(29) =< -V2+1
aux(37) =< V
aux(38) =< 2*V
s(62) =< aux(14)
s(41) =< aux(15)
s(18) =< aux(38)
s(5) =< aux(17)
s(4) =< aux(18)
aux(31) =< aux(37)
it(29) =< aux(37)
it(30) =< aux(37)
it(35) =< aux(37)
it(30) =< aux(38)
it(35) =< aux(38)
aux(24) =< aux(21)+1
s(143) =< aux(37)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(37)+aux(29)
it(35) =< aux(37)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
with precondition: [Out=0,V>=2,V2>=0]
* Chain [[29,30,31,35],40]: 8*it(29)+11*it(30)+6*it(35)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+18*s(160)+2*s(166)+2*s(169)+6
Such that:aux(48) =< 1
aux(21) =< V+V2
aux(49) =< V/2+V2
aux(50) =< V/2+V2+1
aux(29) =< -V2+1
aux(51) =< V
aux(52) =< 2*V
s(169) =< aux(49)
s(166) =< aux(50)
s(160) =< aux(48)
aux(31) =< aux(51)
it(29) =< aux(51)
it(30) =< aux(51)
it(35) =< aux(51)
it(30) =< aux(52)
it(35) =< aux(52)
aux(24) =< aux(21)+1
s(143) =< aux(51)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(51)+aux(29)
it(35) =< aux(51)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(52)
with precondition: [Out=0,V>=2,V2>=0]
* Chain [[29,30,31,35],39]: 8*it(29)+11*it(30)+6*it(35)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+2*s(182)+1*s(184)+6
Such that:aux(53) =< 1
aux(21) =< V+V2
aux(29) =< -V2+1
s(184) =< Out+1
aux(54) =< V
aux(55) =< 2*V
s(182) =< aux(53)
aux(31) =< aux(54)
it(29) =< aux(54)
it(30) =< aux(54)
it(35) =< aux(54)
it(30) =< aux(55)
it(35) =< aux(55)
aux(24) =< aux(21)+1
s(143) =< aux(54)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(54)+aux(29)
it(35) =< aux(54)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(55)
with precondition: [V>=2,V2>=0,Out>=1,V+2*V2>=2*Out]
* Chain [[29,30,31,35],38]: 8*it(29)+11*it(30)+6*it(35)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+2*s(185)+1*s(187)+5
Such that:aux(56) =< 1
aux(21) =< V+V2
s(187) =< V/2+V2
aux(29) =< -V2+1
aux(57) =< V
aux(58) =< 2*V
s(185) =< aux(56)
aux(31) =< aux(57)
it(29) =< aux(57)
it(30) =< aux(57)
it(35) =< aux(57)
it(30) =< aux(58)
it(35) =< aux(58)
aux(24) =< aux(21)+1
s(143) =< aux(57)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(57)+aux(29)
it(35) =< aux(57)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(58)
with precondition: [V>=2,V2>=0,Out>=0,V+2*V2>=2*Out+2]
* Chain [[29,30,31,35],37]: 8*it(29)+11*it(30)+6*it(35)+3*s(143)+24*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+4*s(195)+4*s(200)+5
Such that:aux(63) =< 1
aux(64) =< 2
aux(21) =< V+V2
aux(29) =< -V2+1
aux(66) =< V
aux(67) =< 2*V
s(200) =< aux(63)
s(195) =< aux(64)
s(144) =< aux(67)
aux(31) =< aux(66)
it(29) =< aux(66)
it(30) =< aux(66)
it(35) =< aux(66)
it(30) =< aux(67)
it(35) =< aux(67)
aux(24) =< aux(21)+1
s(143) =< aux(66)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(66)+aux(29)
it(35) =< aux(66)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
with precondition: [Out=0,V>=2,V2>=0]
* Chain [[29,30,31,35],36,42]: 8*it(29)+11*it(30)+6*it(35)+24*s(4)+24*s(5)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+11
Such that:aux(68) =< 1
aux(69) =< 2
aux(21) =< V+V2
aux(29) =< -V2+1
aux(70) =< V
aux(71) =< 2*V
s(5) =< aux(68)
s(4) =< aux(69)
aux(31) =< aux(70)
it(29) =< aux(70)
it(30) =< aux(70)
it(35) =< aux(70)
it(30) =< aux(71)
it(35) =< aux(71)
aux(24) =< aux(21)+1
s(143) =< aux(70)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(70)+aux(29)
it(35) =< aux(70)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(71)
with precondition: [Out=0,V>=4,V2>=0]
* Chain [[29,30,31,35],36,41]: 8*it(29)+11*it(30)+6*it(35)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+3*s(212)+3*s(213)+12
Such that:aux(74) =< 1
aux(75) =< 2
aux(21) =< V+V2
aux(29) =< -V2+1
aux(76) =< V
aux(77) =< 2*V
s(212) =< aux(74)
s(213) =< aux(75)
aux(31) =< aux(76)
it(29) =< aux(76)
it(30) =< aux(76)
it(35) =< aux(76)
it(30) =< aux(77)
it(35) =< aux(77)
aux(24) =< aux(21)+1
s(143) =< aux(76)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(76)+aux(29)
it(35) =< aux(76)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(77)
with precondition: [Out=1,V>=4,V2>=0]
* Chain [[29,30,31,35],34,42]: 8*it(29)+11*it(30)+6*it(35)+24*s(4)+13*s(41)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+10
Such that:aux(79) =< 1
aux(80) =< 2
aux(21) =< V+V2
aux(29) =< -V2+1
aux(81) =< V
aux(82) =< 2*V
s(4) =< aux(79)
s(41) =< aux(80)
aux(31) =< aux(81)
it(29) =< aux(81)
it(30) =< aux(81)
it(35) =< aux(81)
it(30) =< aux(82)
it(35) =< aux(82)
aux(24) =< aux(21)+1
s(143) =< aux(81)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(81)+aux(29)
it(35) =< aux(81)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(82)
with precondition: [Out=0,V>=4,V2>=0]
* Chain [[29,30,31,35],34,41]: 8*it(29)+11*it(30)+6*it(35)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+3*s(214)+1*s(223)+11
Such that:aux(83) =< 1
s(223) =< 2
aux(21) =< V+V2
aux(29) =< -V2+1
aux(84) =< V
aux(85) =< 2*V
s(214) =< aux(83)
aux(31) =< aux(84)
it(29) =< aux(84)
it(30) =< aux(84)
it(35) =< aux(84)
it(30) =< aux(85)
it(35) =< aux(85)
aux(24) =< aux(21)+1
s(143) =< aux(84)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(84)+aux(29)
it(35) =< aux(84)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(85)
with precondition: [Out=1,V>=4,V2>=0]
* Chain [[29,30,31,35],34,37]: 8*it(29)+11*it(30)+6*it(35)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+5*s(195)+5*s(200)+10
Such that:aux(86) =< 1
aux(87) =< 2
aux(21) =< V+V2
aux(29) =< -V2+1
aux(88) =< V
aux(89) =< 2*V
s(200) =< aux(86)
s(195) =< aux(87)
aux(31) =< aux(88)
it(29) =< aux(88)
it(30) =< aux(88)
it(35) =< aux(88)
it(30) =< aux(89)
it(35) =< aux(89)
aux(24) =< aux(21)+1
s(143) =< aux(88)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(88)+aux(29)
it(35) =< aux(88)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(89)
with precondition: [Out=0,V>=4,V2>=0]
* Chain [[29,30,31,35],33,42]: 8*it(29)+11*it(30)+6*it(35)+11*s(4)+12*s(5)+13*s(41)+13*s(62)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+11
Such that:aux(90) =< 1
aux(91) =< 2
aux(21) =< V+V2
aux(92) =< V/2+V2
aux(18) =< V/2+V2+1
aux(29) =< -V2+1
aux(93) =< V
aux(94) =< 2*V
s(62) =< aux(90)
s(41) =< aux(91)
s(5) =< aux(92)
s(4) =< aux(18)
aux(31) =< aux(93)
it(29) =< aux(93)
it(30) =< aux(93)
it(35) =< aux(93)
it(30) =< aux(94)
it(35) =< aux(94)
aux(24) =< aux(21)+1
s(143) =< aux(93)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(93)+aux(29)
it(35) =< aux(93)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(94)
with precondition: [Out=0,V>=4,V2>=0]
* Chain [[29,30,31,35],33,41]: 8*it(29)+11*it(30)+6*it(35)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+2*s(214)+3*s(215)+1*s(224)+1*s(225)+12
Such that:s(224) =< 1
s(225) =< 2
aux(21) =< V+V2
aux(95) =< V/2+V2
aux(73) =< V/2+V2+1
aux(29) =< -V2+1
aux(96) =< V
aux(97) =< 2*V
s(215) =< aux(95)
s(214) =< aux(73)
aux(31) =< aux(96)
it(29) =< aux(96)
it(30) =< aux(96)
it(35) =< aux(96)
it(30) =< aux(97)
it(35) =< aux(97)
aux(24) =< aux(21)+1
s(143) =< aux(96)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(96)+aux(29)
it(35) =< aux(96)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(97)
with precondition: [Out=1,V>=4,V2>=0]
* Chain [[29,30,31,35],32,42]: 8*it(29)+11*it(30)+6*it(35)+23*s(4)+13*s(41)+13*s(62)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+10
Such that:aux(98) =< 1
aux(99) =< 2
aux(21) =< V+V2
aux(29) =< -V2+1
aux(101) =< V
aux(102) =< 2*V
aux(103) =< V/2+V2
s(62) =< aux(98)
s(41) =< aux(99)
s(4) =< aux(103)
aux(31) =< aux(101)
it(29) =< aux(101)
it(30) =< aux(101)
it(35) =< aux(101)
it(30) =< aux(102)
it(35) =< aux(102)
aux(24) =< aux(21)+1
s(143) =< aux(101)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(101)+aux(29)
it(35) =< aux(101)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(102)
with precondition: [Out=0,V>=4,V2>=0]
* Chain [[29,30,31,35],32,41]: 8*it(29)+11*it(30)+6*it(35)+3*s(143)+8*s(144)+1*s(145)+1*s(150)+1*s(156)+1*s(157)+5*s(214)+1*s(227)+1*s(228)+11
Such that:s(227) =< 1
s(228) =< 2
aux(21) =< V+V2
aux(29) =< -V2+1
aux(105) =< V
aux(106) =< 2*V
aux(107) =< V/2+V2
s(214) =< aux(107)
aux(31) =< aux(105)
it(29) =< aux(105)
it(30) =< aux(105)
it(35) =< aux(105)
it(30) =< aux(106)
it(35) =< aux(106)
aux(24) =< aux(21)+1
s(143) =< aux(105)*2
s(145) =< it(29)*aux(21)
aux(31) =< aux(105)+aux(29)
it(35) =< aux(105)+aux(29)
s(150) =< it(30)*aux(24)
s(157) =< aux(31)*2
s(156) =< aux(31)
s(144) =< aux(106)
with precondition: [Out=1,V>=4,V2>=0]
* Chain [42]: 11*s(4)+11*s(5)+48*s(18)+12*s(41)+12*s(62)+5
Such that:aux(14) =< 1
aux(15) =< 2
aux(16) =< V
aux(17) =< V2
aux(18) =< V2+1
s(62) =< aux(14)
s(41) =< aux(15)
s(18) =< aux(16)
s(5) =< aux(17)
s(4) =< aux(18)
with precondition: [Out=0,V>=0,V2>=0]
* Chain [41]: 2*s(214)+2*s(215)+6
Such that:aux(72) =< V2
aux(73) =< V2+1
s(215) =< aux(72)
s(214) =< aux(73)
with precondition: [V=0,Out=1,V2>=0]
* Chain [40]: 18*s(160)+2*s(166)+2*s(169)+6
Such that:aux(48) =< 1
aux(49) =< V2
aux(50) =< V2+1
s(169) =< aux(49)
s(166) =< aux(50)
s(160) =< aux(48)
with precondition: [V=1,Out=0,V2>=0]
* Chain [39]: 2*s(182)+1*s(184)+6
Such that:s(184) =< V2+1
aux(53) =< 1
s(182) =< aux(53)
with precondition: [V=1,V2=Out,V2>=1]
* Chain [38]: 2*s(185)+1*s(187)+5
Such that:s(187) =< V2
aux(56) =< 1
s(185) =< aux(56)
with precondition: [V=1,Out>=0,V2>=Out+1]
* Chain [37]: 16*s(188)+4*s(195)+4*s(200)+5
Such that:aux(63) =< 1
aux(64) =< 2
aux(65) =< V
s(200) =< aux(63)
s(195) =< aux(64)
s(188) =< aux(65)
with precondition: [V2=0,Out=0,V>=0]
* Chain [36,42]: 24*s(4)+24*s(5)+11
Such that:aux(68) =< 1
aux(69) =< 2
s(5) =< aux(68)
s(4) =< aux(69)
with precondition: [V2=0,Out=0,V>=2]
* Chain [36,41]: 3*s(212)+3*s(213)+12
Such that:aux(74) =< 1
aux(75) =< 2
s(212) =< aux(74)
s(213) =< aux(75)
with precondition: [V2=0,Out=1,V>=2]
* Chain [34,42]: 24*s(4)+13*s(41)+10
Such that:aux(79) =< 1
aux(80) =< 2
s(4) =< aux(79)
s(41) =< aux(80)
with precondition: [Out=0,V>=2,V2>=0]
* Chain [34,41]: 3*s(214)+1*s(223)+11
Such that:s(223) =< 2
aux(83) =< 1
s(214) =< aux(83)
with precondition: [Out=1,V>=2,V2>=0]
* Chain [34,37]: 5*s(195)+5*s(200)+10
Such that:aux(86) =< 1
aux(87) =< 2
s(200) =< aux(86)
s(195) =< aux(87)
with precondition: [Out=0,V>=2,V2>=0]
* Chain [33,42]: 11*s(4)+12*s(5)+13*s(41)+13*s(62)+11
Such that:aux(18) =< V2+2
aux(90) =< 1
aux(91) =< 2
aux(92) =< V2+1
s(62) =< aux(90)
s(41) =< aux(91)
s(5) =< aux(92)
s(4) =< aux(18)
with precondition: [Out=0,V>=2,V2>=1]
* Chain [33,41]: 2*s(214)+3*s(215)+1*s(224)+1*s(225)+12
Such that:s(224) =< 1
s(225) =< 2
aux(73) =< V2+2
aux(95) =< V2+1
s(215) =< aux(95)
s(214) =< aux(73)
with precondition: [Out=1,V>=2,V2>=1]
* Chain [32,42]: 11*s(4)+12*s(5)+13*s(41)+13*s(62)+10
Such that:aux(18) =< V2+1
aux(98) =< 1
aux(99) =< 2
aux(100) =< V2
s(62) =< aux(98)
s(41) =< aux(99)
s(5) =< aux(100)
s(4) =< aux(18)
with precondition: [Out=0,V>=2,V2>=1]
* Chain [32,41]: 2*s(214)+3*s(215)+1*s(227)+1*s(228)+11
Such that:s(227) =< 1
s(228) =< 2
aux(73) =< V2+1
aux(104) =< V2
s(215) =< aux(104)
s(214) =< aux(73)
with precondition: [Out=1,V>=2,V2>=1]
#### Cost of chains of start(V,V2,V11,V12):
* Chain [43]: 31*s(560)+44*s(561)+789*s(574)+553*s(575)+176*s(578)+46*s(579)+154*s(581)+84*s(582)+42*s(584)+14*s(585)+14*s(586)+14*s(587)+14*s(588)+176*s(589)+27*s(590)+11*s(591)+13*s(592)+356*s(654)+33*s(655)+1*s(658)+46*s(681)+308*s(683)+84*s(684)+84*s(686)+14*s(687)+14*s(688)+14*s(689)+14*s(690)+352*s(691)+27*s(692)+11*s(693)+44*s(752)+46*s(770)+84*s(773)+14*s(776)+14*s(777)+14*s(778)+14*s(779)+27*s(781)+11*s(782)+13*s(783)+13
Such that:s(658) =< V+1
s(664) =< V/2+2
s(753) =< V/2+V2+2
s(562) =< V11/2+V12+2
aux(139) =< 1
aux(140) =< 2
aux(141) =< V
aux(142) =< V+V2
aux(143) =< 2*V
aux(144) =< V/2
aux(145) =< V/2+1
aux(146) =< V/2+V2
aux(147) =< V/2+V2+1
aux(148) =< -V2+1
aux(149) =< V2
aux(150) =< V2+1
aux(151) =< V2+2
aux(152) =< V11
aux(153) =< V11+V12
aux(154) =< 2*V11
aux(155) =< V11/2+V12
aux(156) =< V11/2+V12+1
aux(157) =< -V12+1
aux(158) =< V12
aux(159) =< V12+1
aux(160) =< V12+2
s(654) =< aux(141)
s(681) =< aux(144)
s(770) =< aux(146)
s(655) =< aux(149)
s(752) =< aux(150)
s(579) =< aux(155)
s(560) =< aux(158)
s(561) =< aux(159)
s(574) =< aux(139)
s(575) =< aux(140)
s(578) =< aux(152)
s(580) =< aux(152)
s(581) =< aux(152)
s(582) =< aux(152)
s(581) =< aux(154)
s(582) =< aux(154)
s(583) =< aux(153)+1
s(584) =< aux(152)*2
s(585) =< s(578)*aux(153)
s(580) =< aux(152)+aux(157)
s(582) =< aux(152)+aux(157)
s(586) =< s(581)*s(583)
s(587) =< s(580)*2
s(588) =< s(580)
s(589) =< aux(154)
s(590) =< aux(156)
s(591) =< s(562)
s(592) =< aux(160)
s(771) =< aux(141)
s(683) =< aux(141)
s(773) =< aux(141)
s(683) =< aux(143)
s(773) =< aux(143)
s(774) =< aux(142)+1
s(686) =< aux(141)*2
s(776) =< s(654)*aux(142)
s(771) =< aux(141)+aux(148)
s(773) =< aux(141)+aux(148)
s(777) =< s(683)*s(774)
s(778) =< s(771)*2
s(779) =< s(771)
s(691) =< aux(143)
s(781) =< aux(147)
s(782) =< s(753)
s(783) =< aux(151)
s(682) =< aux(141)
s(684) =< aux(141)
s(684) =< aux(143)
s(685) =< aux(141)+1
s(687) =< s(654)*aux(141)
s(682) =< aux(141)+aux(139)
s(684) =< aux(141)+aux(139)
s(688) =< s(683)*s(685)
s(689) =< s(682)*2
s(690) =< s(682)
s(692) =< aux(145)
s(693) =< s(664)
with precondition: []
Closed-form bounds of start(V,V2,V11,V12):
-------------------------------------
* Chain [43] with precondition: []
- Upper bound: nat(V)*1112+1908+nat(V)*28*nat(V)+nat(V2)*33+nat(V11)*554+nat(V12)*31+nat(2*V)*352+nat(2*V11)*176+nat(V+V2)*28*nat(V)+nat(V+1)+nat(V2+1)*44+nat(V2+2)*13+nat(V11+V12)*28*nat(V11)+nat(V12+1)*44+nat(V12+2)*13+nat(V/2+V2+1)*27+nat(V/2+V2+2)*11+nat(V11/2+V12+1)*27+nat(V11/2+V12+2)*11+nat(V/2+V2)*46+nat(V/2+1)*27+nat(V/2+2)*11+nat(V11/2+V12)*46+nat(V/2)*46
- Complexity: n^2
### Maximum cost of start(V,V2,V11,V12): nat(V)*1112+1908+nat(V)*28*nat(V)+nat(V2)*33+nat(V11)*554+nat(V12)*31+nat(2*V)*352+nat(2*V11)*176+nat(V+V2)*28*nat(V)+nat(V+1)+nat(V2+1)*44+nat(V2+2)*13+nat(V11+V12)*28*nat(V11)+nat(V12+1)*44+nat(V12+2)*13+nat(V/2+V2+1)*27+nat(V/2+V2+2)*11+nat(V11/2+V12+1)*27+nat(V11/2+V12+2)*11+nat(V/2+V2)*46+nat(V/2+1)*27+nat(V/2+2)*11+nat(V11/2+V12)*46+nat(V/2)*46
Asymptotic class: n^2
* Total analysis performed in 1780 ms.